T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
e'<e.@e'(xes-when(es; x; e))  e''(e',e].es-when(es; x; e'') = es-when(es; x; e)  T
 e'e.es-when(es; x; e') = es-when(es; x; e)  T 

latex

Definitions	A c B, x. t(x), guard(T), P  Q, True, T, P  Q, es-dtype(es; i; x; T), prop{i:l}, t  T, x:A. B(x), x(s), SqStable(P), P  Q, P  Q, P  Q
Lemmas	alle-le wf, es-first wf, not wf, alle-between3 wf, es-when wf, es-change-to wf, existse-before wf, es-vartype wf, sq stable subtype rel, es-isconst wf, sq stable from decidable, decidable assert, eqof wf, assert wf, decidable functionality, deq property, deq wf, event system wf, Id wf, es-loc wf, es-dtype wf, es-E wf, change-to-lemma